Nuprl Lemma : qmul_over_minus_qrng
11,40
postcript
pdf
a
,
b
:
. ((-(
a
)) *
b
) = -(
a
*
b
)
& (
a
* -(
b
)) = -(
a
*
b
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
-
r
,
*
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
Lemmas
crng
wf
,
qrng
wf
,
rng
times
over
minus
origin
a, b:
. ((-(a)) * b) = -(a * b) 
& (a * -(b)) = -(a * b) a, b:. ((-(a)) * b) = -(a * b) & (a * -(b)) = -(a * b) T+*>x:A. B(x)